…ules) (#205)

docs(formal): remove the duplicated Set Printing Width comment (9
modules)

#202 landed the same three-line explanatory comment twice in every
module —
once above `Set Printing Width 400.` where it belongs, and once orphaned
immediately below it. My fault: I ran the insertion, then deleted only
the
`Set Printing Width 400.` line to A/B-test whether the ~78-column wrap
was
actually hiding any axiom from the guard, then re-ran the insertion. The
sed
that undid the test matched only the directive, not its comment, so the
second
pass stacked a fresh copy on top of the leftover.

Comment-only; no directive, no proof and no guard changes.
`formal/Justfile`
is untouched.

To be accurate about scope, since the obvious worry is that a text edit
near
the imports clipped something: it did not. `Import ListNotations.` and
every
`Require Import` are intact in all nine modules — verified before and
after.
(A *different* cleanup attempt of mine did briefly eat that import by
skipping
a fixed three lines past the marker, which in `Planner.v` overran the
comment.
That version was reset and never committed; it is mentioned only so the
next
person knows the offset-based approach is the wrong tool here. This
commit
removes the second matched block specifically, keyed on occurrence
count.)

Verified: real coqc 8.20.1 -> `check-assumptions` exits 0, 9/9 OK; stub
coqc
-> exit 127, so the gate from #202 still fails when it should;
`Normalizer.out`
still prints at 157 columns, so the wrap fix is unaffected; `reuse lint`
compliant.

…n both modules (#206)

feat(formal): discharge optimize_is_permutation — axiom to theorem, in
both modules

`optimize_is_permutation` was an `Axiom` in `formal/Planner.v` and,
separately,
a second identical `Axiom` in `formal/PlannerSemantic.v`. Both are now
gone.

**It was not merely unproven — it was unprovable.** `optimize` was a
`Parameter`, so nothing constrained it: `fun _ => []` inhabits the
parameter and
refutes `forall lp, Permutation lp (optimize lp)`. Assuming the
statement was
assuming the conclusion, and no amount of proof effort against that
signature
would have worked. Discharging it *requires* replacing the parameter
with a
definition, which is what this does:

* `modality` becomes an `Inductive` with the six constructors of
`crate::Modality`, and `execution_priority` transcribes the Rust match
arms
(Temporal 10, Vector 20, Document 30, Graph 40, Tensor 50, Semantic 90).
* `optimize` becomes `Coq.Sorting.Mergesort`'s `sort` under `node_leb` —
  execution priority first, cost as tie-breaker, i.e. the key
  `Optimizer::optimize`'s `sort_by` comparator actually uses.
* The permutation property falls out of the standard library's
`Permuted_sort`,
  which is itself closed under the global context.

All five call sites were left untouched and still compile: the theorem
statement is character-for-character what the axiom asserted.

`PlannerSemantic.v` claimed in a comment to be "reusing Planner.v
abstractions"
while in fact re-declaring its own `modality`, `condition`, `node`,
`optimize`
and a duplicate axiom. The two files agreed only by coincidence, and the
duplicate meant discharging Planner's axiom would have left an identical
assumption standing next door. It now genuinely `Require Import
Planner`, and
`formal/Justfile` gains the `planner-semantic: planner` dependency edge
that
this makes necessary.

**Whitelists tightened — this is the acceptance test, not bookkeeping.**
The
guards enforce "exactly these assumptions", never "no assumptions", so
leaving
`optimize_is_permutation` listed would have let it return silently:

* Planner: `modality|condition|optimize|optimize_is_permutation` ->
`condition|node_cost`
* PlannerSemantic: drops `modality`, `optimize`,
`optimize_is_permutation`

Both `formal/Justfile` and `.github/workflows/coq-build.yml` updated
together.

Two `Parameter`s remain **by design**, and being parametric in them
makes the
result stronger, not weaker — it holds for *any* condition
representation and
*any* cost function: `condition` (the Rust `ConditionKind`'s nine
constructors
are irrelevant to whether nodes are reordered or lost) and `node_cost`
(abstracts `CostModel::estimate`'s `time_ms`).

Two honest model-vs-code gaps, both recorded in the module header rather
than
elided, neither affecting the permutation property:

* `node_cost` returns `nat`; the Rust tie-breaker is `f64` compared with
  `partial_cmp(...).unwrap_or(Equal)`. A NaN would make that comparator
non-transitive and violate `sort_by`'s contract. NaN is unreachable
today —
the only division in `CostModel::estimate` is guarded and feeds
`selectivity`,
  not `time_ms` — but nothing in the Rust types enforces that.
* Rust `optimize` is partial (`PlannerError::EmptyPlan`); `sort []` is
`[]`.

`exec_node_comm` deliberately stays. It is a genuine spec axiom over an
uninterpreted `exec_node` and needs per-operator semantics to discharge
— not
something this change touches, and it should not look like collateral.

Verified:
* Clean build: `just -f formal/Justfile all` and `check-assumptions`
both exit 0,
  9/9 OK, with the tightened whitelists.
* `optimize_is_permutation` appears zero times in either module's
`Print Assumptions` output, and no `Axiom optimize_is_permutation`
remains
  anywhere (was 2).
* **Negative control** — reintroducing an axiom a theorem depends on is
caught:
`ERROR(Planner): unexpected axiom: sneaky_regression`, gate exit 1. The
  tightened whitelist genuinely fails rather than passing vacuously.
* Stub `coqc` still drives the gate to exit 127, so #202's fix is
intact.
* `reuse lint` compliant.